NIL 

* 

TYPE-AXIOMS: 

TYPE-HYPOTHESES: 
TYPE-THEOREM: 
7 ELEMENT(THM50(AX48(X1,X2)),X1) 
8 ELEMENT(THM50(AX48(X1,X2)),X2) 
9 ELEMENT(THM50(X1),AX48(X1,X2)) ¬ELEMENT(THM50(X1),X2) 
10 ELEMENT(THM50(X1),AX48(X2,X1)) ¬ELEMENT(THM50(X1),X2) 
11 ¬ELEMENT(THM50(X1),AX49(X1)) 
12 ¬ELEMENT(THM50(AX49(X1)),X1) 
COUNT 
6 
LEVEL 
1 
ELAPSED-TIME 
2300 
13 ELEMENT(THM50(AX48(X1,X2)),AX48(X1,X3)) ¬ELEMENT(THM50(AX48(X1,X2)),X3) 
14 ELEMENT(THM50(AX48(X1,X2)),AX48(X3,X1)) ¬ELEMENT(THM50(AX48(X1,X2)),X3) 
15 ELEMENT(THM50(AX48(X1,X2)),AX48(X2,X3)) ¬ELEMENT(THM50(AX48(X1,X2)),X3) 
16 ELEMENT(THM50(AX48(X1,X2)),AX48(X3,X2)) ¬ELEMENT(THM50(AX48(X1,X2)),X3) 
17 ¬ELEMENT(THM50(AX48(X1,X2)),AX49(X1)) 
18 ¬ELEMENT(THM50(AX48(X1,X2)),AX49(X2)) 
19 ELEMENT(THM50(X1),AX48(X1,X1)) 
20 ELEMENT(THM50(AX48(X1,X2)),AX48(AX48(X1,X2),X1)) 
21 ELEMENT(THM50(AX48(X1,X2)),AX48(X1,AX48(X1,X2))) 
22 ELEMENT(THM50(AX48(X1,X2)),AX48(AX48(X1,X2),X2)) 
23 ELEMENT(THM50(AX48(X1,X2)),AX48(X2,AX48(X1,X2))) 
COUNT 
35 
LEVEL 
2 
ELAPSED-TIME 
6383 
24 ELEMENT(THM50(X1),AX48(AX48(X1,X1),X2)) ¬ELEMENT(THM50(X1),X2) 
25 ELEMENT(THM50(X1),AX48(X2,AX48(X1,X1))) ¬ELEMENT(THM50(X1),X2) 
26 ¬ELEMENT(THM50(X1),AX49(AX48(X1,X1))) 
27 ELEMENT(THM50(AX48(X1,X2)),AX48(X1,X1)) 
28 ELEMENT(THM50(AX48(X1,X2)),AX48(X2,X1)) 
NIL 1 2
1 ELEMENT(THM50(AX48(X1,X2)),X1) 3 8
2 ¬ELEMENT(THM50(AX48(X1,X2)),AX49(X2)) 5 6
3 ELEMENT(X1,X2) ¬ELEMENT(X1,AX48(X2,X3)) ¬SET(X1) AX 1
5 ¬ELEMENT(X1,X2) ¬ELEMENT(X1,AX49(X2)) ¬SET(X1) AX 4
6 ELEMENT(THM50(AX48(X1,X2)),X2) 7 8
7 ELEMENT(X1,X2) ¬ELEMENT(X1,AX48(X3,X2)) ¬SET(X1) AX 2
8 ELEMENT(THM50(X1),X1) THM 2
NIL